ecl-es-act(es; m; x)
== ecl_ind(x;
== ecl_ind(k,test.(e1,e2. False);
== ecl_ind(a,b,aa,ab.(e1,e2. (aa(e1,e2))
== ecl_ind( e(e1,e2].(ecl-es-halt(es; a)(0,e1,es-pred(es; e)))  (ab(e,e2)));
== ecl_ind(a,b,aa,ab.(e1,e2. ((aa(e1,e2))
== ecl_ind( l-all(ecl-ex(b); n.e[e1,e2).(ecl-es-halt(es; b)(n,e1,e))))
== ecl_ind( ((ab(e1,e2))  l-all(ecl-ex(a); n.e[e1,e2).(ecl-es-halt(es; a)(n,e1,e)))));
== ecl_ind(a,b,aa,ab.(e1,e2. ((aa(e1,e2))
== ecl_ind( l-all(cons(0; ecl-ex(b)); n.e[e1,e2).(ecl-es-halt(es; b)(n,e1,e))))
== ecl_ind( ((ab(e1,e2))  l-all(cons(0; ecl-ex(a)); n.e[e1,e2).(ecl-es-halt(es; a)(n,e1,e)))));
== ecl_ind(a,aa.(e1,e2. [e1;e2]~([x,y].ecl-es-halt(es; a)(0,x,y))*[x,y].aa(x,y));
== ecl_ind(a,n,aa.if (m = n) then ecl-es-halt(es; a)(0) else aa fi ;
== ecl_ind(a,n,aa.aa;
== ecl_ind(a,l,aa.aa) 

latex

---

clarification:

ecl-es-act(es; m; x)
== ecl_ind(x;
== ecl_ind(k,test.(e1,e2. False);
== ecl_ind(a,b,aa,ab.(e1,e2. (aa(e1,e2))
== ecl_ind( existse-between3(es;e1;e2;e.(ecl-es-halt(es; a)(0,e1,es-pred(es; e)))  (ab(e,e2))));
== ecl_ind(a,b,aa,ab.(e1,e2. ((aa(e1,e2))
== ecl_ind( l-all(ecl-ex(b); n.alle from es in [e1;e2).(ecl-es-halt(es; b)(n,e1,e))))
== ecl_ind( ((ab(e1,e2))
== ecl_ind(  l-all(ecl-ex(a); n.alle from es in [e1;e2).(ecl-es-halt(es; a)(n,e1,e)))));
== ecl_ind(a,b,aa,ab.(e1,e2. ((aa(e1,e2))
== ecl_ind( l-all(cons(0; ecl-ex(b)); n.alle from es in [e1;e2).(ecl-es-halt(es; b)(n,e1,e))))
== ecl_ind( ((ab(e1,e2))
== ecl_ind(  l-all(cons(0; ecl-ex(a)); n.alle from es in [e1;e2).(ecl-es-halt(es; a)(n,e1,e)))));
== ecl_ind(a,aa.(e1,e2. es-pstar-q(es;x,y.ecl-es-halt(es; a)(0,x,y);x,y.aa(x,y);e1;e2));
== ecl_ind(a,n,aa.if (m = n) then ecl-es-halt(es; a)(0) else aa fi ;
== ecl_ind(a,n,aa.aa;
== ecl_ind(a,l,aa.aa) 

latex

Definitions	#$n, ecl-es-halt(es; x), f(a), (i = j), if b then t else f fi , [e1;e2]~([a,b].p(a;b))*[a,b].q(a;b), x.A(x), A, e[e1,e2).P(e), ecl-ex(x), cons(car; cdr), l-all(L; x.P(x)), P  Q, P  Q, es-pred(es; e), e(e1,e2].P(e), False, ecl ind
FDL editor aliases	ecl-es-act